COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.sec(LCF: Logic for Computable Functions)
C00005 00003	.ss(Deduction,,)
C00015 00004	.SS(Complete Partial Orders,,)
C00022 00005	.SS(The Models,,)
C00038 00006	.end "on |]"
C00039 ENDMK
C⊗;
.sec(LCF: Logic for Computable Functions)
.SS(Introduction,,)
.begin indent 10,10,10;
"...formalism without eventual interpretation is in the end useless.  Now it may
turn out that a system such as the ?λ-calculus will have an interpretation along
standard lines (and I have spent more days than I care to remember trying to
find one), but until it is produced I would like to argue that its purposes
can just as well be fulfilled by a system involving types."
.end


This statement by D. Scott was written in an unpublished memorandum [12] about
September of 1969, just a couple of months before he discovered the models for
the ?λ-calculus.  It was in this paper that he proposed LCF, a deductive system
for computable functions.

LCF is a version of the typed ?λ-calculus, its models are simpler, but its syntax
is more complex.  Having already looked at the type-free ?λ-calculus, we have some
familiarity with ?λ-terms, the addition of types is merely a restriction on
what kinds of arguments a function may take.

.ss(Deduction,,)
First, we describe the formal system of LCF.
.begin tabit1(10);

%71.%1 Countable set of symbols:
\identifiers: ⊗T, ⊗F, ⊗U, ⊃, ⊗Y, ∪x, y, ?x1, ?y1, ...
\type symbols: ⊗i, ⊗t
\predicate symbols: ≤, $ε
\auxiliary symbols: ?λ, ∪.∩, [, ], (, ), ,, →, :
.end
We use "≡" as syntactic identity, and "∪x=y∩" as an abbreviation for
"∪x∩≤∪y∩ and ∪y∩≤∪x∩".
We use β, β1, β2, ... as meta-variables over types.
 

%72∩.  The terms of LCF are those of a typed ?λ-calculus.
.begin nofill;
	1)  ⊗i and ⊗t are (ground) types.
	2)  If β1, β2 are types, then (β1→β2) is a type.
.end
We use β, β1, β2, ... to denote types, and omit parentheses according to the
convention that "→" associates to the right, so that β1→β2→β3 is an abbreviation
for (β1→(β2→β3)).  (Shades of Sch⊗onfinkeling again!)

Each term has a well-defined type.  We use ?s, ?t, ?u to denote terms, and write
?s:β to mean ?s is a term of type β.
.begin indent 10,10;
1)  Any identifier is an %3atomic term%1.  There are infinitely many identifiers 
of each type, the type of each is determined in some way (following a ":" or
possibly by subscripting), and they include ⊗T:⊗t, ⊗F:⊗t and the families
(indexed by type) ⊗U↓β, ⊃↓tβ, and ⊗Y↓3β.  These identifiers are special only
in that each "standard interpretation" will assign a particular element to each
of them.  We use ?x and ?y to denote arbitrary identifiers.

2)  If ?s:β1→β2 and ?t:β1 are terms, then ∪s(t)∩:β2 (also written "∪(st)∩") 
is a %3term%1.

3)  If ?x:β1 is an identifier and ?s:β2 is a term, then (∪λx.s∩):β1→β2 is a %3term∩.
.end

If ?s:β, ?t:β are terms, then ∪s∩≤∪t∩ is an %3atomic well-formed formula∩ (⊗→awff↔←).
A %3well-formed formula∩ (wff) is a set of awffs.  We use πP, πQ, πP1, πQ1, πP2, πQ2, ...
to denote arbitrary wffs.  
If πP and πQ are wffs, then πP$επQ is a sentence.  If πP is the empty set, we
just write $επQ⊗↓In previous sections we have used "$ε" as a symbol denoting
"provability". Here it is a formal symbol of LCF; for ease in reading we may
anticipate the interpretation of it as an implication between wffs, 
and read "πP$επQ" as
"if πP, then πQ".  The symbol "##", which was used as an implication before, is
now an identifier which will represent the "conditional expression", that is,
##∪(s)(t)(u)∩ may be read "if#?s#then#?t,#else#∪u∩".←.

.begin nofill;

%73. ∩and∪ 4.∩  Axioms and Rules of Inference
.end
Axioms can be considered as rules of inference with no premises.  We list all of
these as rules of inference and name them in order to be able to refer to them
later.  We write the hypotheses of each rule above a dotted line, with the
conclusion written below.  If there are no hypotheses, we omit the line.

In specifying the inference rules we use [∪t/x∩]πP to mean, as before: substitution of ?t
for all free occurrences of ?x in πP, with suitable changes of bound variables
so that no identifier free in ?t becomes bound after the substitution.

.begin tabit2 (10,25)
\INCL\πP$επQ     (where πQ is a subset of πP)

.group
\\πP$επQ1   πP$επQ2
\CONJ\--------------      (πll is ordinary set union)
\\   πP $ε πQ1πllπQ2
.apart
.group

\\πP1$επP2   πP2$επP3
\CUT\----------------
\\   πP1$επP3
.apart

\APPL\∪t∩≤∪u $ε ∪s(t)∩≤∪s(u)∩

\REFL\$ε∪s∩≤∪s∩

\TRANS\∪s∩≤∪t, t∩≤∪u $ε ∪s∩≤∪u∩

\MIN1\$ε ⊗U∪∩≤∪s∩

\MIN2\$ε ⊗U∪(s)∩≤∪∩⊗U

.begin fill;
In the last two rules we have omitted the type subscripts from ⊗U, intending
that they be supplied in such a way as to yield a proper awff, that is, terms
on either side of "≤" should have the same type.  We could have written
#$ε⊗U%4β1→β2∩(?s:β1)≤⊗U%4β2∩.  Similarly, we will omit subscripts from ⊃ and
⊗Y.
.end

\CONDT\$ε ⊃(⊗T)∪(s)(t)=s∩

\CONDU\$ε ⊃(⊗U)∪(s)(t)=⊗U

\CONDF\$ε ⊃(⊗F)∪(s)(t)=t∩

.group
\\    πP$ε∪s∩≤∪t∩
\ABSTR\----------------   (?x not free in πP)
\\πP$ε∪(λx.s)∩≤∪(λx.t)∩
.apart

\CONV\$ε ∪(λx.s)(t)=[t/x]s∩

\ETACONV\$ε ∪(λx.y(x))=y∩  (?y distinct from ?x)

.group
\\πP, ?s=⊗T $ε πQ    πP, ?s=⊗U $ε πQ    πP, ?s=⊗F $ε πQ
\CASES\------------------------------------------
\\                    πP $ε πQ
.apart

\FIXP\$ε ∪Y(x)=x(Y(x))∩

.begin turnoff "∪";group
\\πP $ε [⊗U/?x]πQ    πPπllπQ $ε [?s(?x)/?x]πQ
\INDUCT\--------------------------------  (?x not free in πP or ?s)
\\       πP $ε [%dY(s)/x∩]πQ
.end
.end

.group
As an example of the use of induction we prove that the "fixed point" ∪Yf∩ is
minimal.⊗↓Any standard interpretation assigns ⊗Y the value of the least fixed point
operator .  We have not yet described a standard interpretation, so use of the
term "fixed point" is a little premature.  However, the proof goes through
merely as a manipulation of symbols regardless of the interpretation of ∪Y∩.←


%7THEOREM 1%1  If ∪s=f(s)∩ then ∪Y(f)∩≤∪s∩,that is, we want to prove
∪s∩≤∪f(s), f(s)∩≤?s $ε ∪Y(f)∩≤?s
.begin nofill; tabit2 (10,53); turnoff "{", "}";
Proof:
\1)  $ε ⊗U≤?s\MIN1 
\2)  ?s≤∪f(s),f(s)∩≤∪s $ε {}\INCL
\3)  ?s≤∪f(s),f(s)∩≤∪s $ε ⊗U≤?s\CUT 2,1
\4)  ∪x∩≤∪s $ε ∪f(x)∩≤∪f(s)∩\APPL
\5)  ?s≤∪f(s),f(s)∩≤∪s, ∪x∩≤?s $ε ?x≤?s\INCL
\6)  ?s≤∪f(s),f(s)∩≤∪s, ∪x∩≤?s $ε ∪f(x)∩≤∪f(s)∩\CUT 4,5
\7)  ?s≤∪f(s),f(s)∩≤∪s, ∪x∩≤?s $ε ∪f(s)∩≤∪s∩\INCL
\8)  ?s≤∪f(s),f(s)∩≤∪s, ∪x∩≤?s $ε ∪f(x)∩≤∪f(s), f(s)∩≤?s∩\CONJ 6,7
\9)  ∪f(x)∩≤∪f(s), f(s)∩≤?s $ε ∪f(x)∩≤?s\TRANS
\10) ?s≤∪f(s),f(s)∩≤∪s, ∪x∩≤?s $ε ∪f(x)∩≤∪s∩\CUT 8,9
\11) ?s≤∪f(s),f(s)∩≤∪s $ε ∪Yf∩≤?s\INDUCT 3, 10
.apart
.end

Remark:  It is interesting to note that %2every∩ term in the typed λ-calculus
has a normal form (as defined in section 5.1).⊗↓A proof may be found in J. H.
Morris's Ph.D. thesis, "Lambda-Calculus Models of Programming Languages",
Massachusetts Institute of Technology, 1968.←  This is surprisingly hard to
prove and does not really concern us here since we are using only the %2terms∩
of typed λ-calculus, the relations between terms in LCF are different.  We have
an entirely different deductive system by way of the rules of inference of LCF.
This fact does give some motivation for Wadsworth's original idea about the
relationships between normal form equivalence and equality in the models for
type-free λ-calculus.



.SS(Complete Partial Orders,,)
In discussing the models for LCF we will be using complete partial orders and
again the concept of a continuous function.

A %3⊗→partial order↔←%1 (⊗→PO↔←) is a pair (πD,π≤) where πD is any domain and π≤ is a
reflexive, transitive, antisymmetric relation over πD.  For a PO (πD, π≤),
a subset πX⊂πD is a %3⊗→chain↔←∩ if
.begin turnoff "{", "}", "|";center;
πX = {πx%4i%1 | i≥0} and πx0π≤πx1π≤πx2π≤...
.end

A PO (πD, π≤) is a %3⊗→complete partial order↔←∩ (⊗→CPO↔←) if
.begin indent 10,10;

1)  It has a minimum element, which we denote by ⊗b%4D∩, or just ⊗b if there is no
confusion.

2)  Every chain πX⊂πD has a least upper bound (lub) in πD, which we denote by πlπX.

.end

(Note that a CPO fails to be a complete lattice only in that it lacks a "top" 
element.)  If πD and πE are CPO's, then a function πf:πD→πE is %3⊗→continuous↔←∩ if
every chain πX⊂πD satisfies
.begin turnoff "{", "}", "|";center;
πl{πf(πx) | πxεπX} = πf(πlπX)
.end

.begin turnoff "{", "}";
Thus a continuous function is one which preserves lubs of chains.  Note that the
set on the left hand side of the above equation is a chain, since if πX={πx0, πx1, ...}
and πx0π≤πx1π≤... then we also have πf(πx0)π≤πf(πx1)π≤... .  To see this, we simply
need observe that %2any∩ continuous function is ⊗→monotonic↔←, i.e., πxπ≤πy => πf(πx)π≤πf(πy),
since if πX is the chain {πxπ≤πy} then πlπX=πy, so we have 
.begin center;
πf(πx) π≤ πl{πf(πx),πf(πy)} = πf(πlπX) = πf(πy).
.end
.end


There is an alternative (more restrictive) definition of CPO's and continuous
functions which uses the concept of a directed set, which we used in
developing the models of the λ-calculus in the previous section.  Here we have
chosen the less restrictive alternative, though the theory can be done with either
definition.

We use the same symbol π≤ for the relation in every PO under discussion, it should
be clear we do not mean for every PO to have the same relation.  We also use names
like πD and πE for both PO's and their domains.  This should cause no 
confusion.  Again, we denote the set of continuous functions from πD to πE by [πD→πE].


%7THEOREM 2%1  If πD and πE are CPO's then πF = [πD→πE] is a CPO under the relation
.begin center;
πfπ≤%2g∩  iff  ∀πxεπD  πf(πx)π≤%2g∩(πx)
.end
Sketch of proof:
.begin indent 10,10;
First, πF is a PO under this relation (check reflexivity,
transitivity, and antisymmetry).

Second, the minimum element ⊗b%4F∩ of πF is easily seen to be ?λπx.⊗b%4E∩.

Finally, we need that any chain πZ⊂πF has a lub πlπZεπF.  Define:
.begin turnoff "{", "}", "|";
.begin center; 
⊗→%fl%2Z∩↔← = ?λπx.πl{πf(πx) | πfεπZ}.
.end
This is well-defined since for each πxεπD, {πf(πx) | πfεπZ} is a chain in πE.  It
is an upper bound since for each πxεπD, πf(πx)#π≤#πl{πf(πx) | πfεπZ}#=#(πlπZ)(πx).  Further
it is a lub, since if πh is any other upper bound for πZ, then for each πxεπD and
πfεπZ we have πf(πx)π≤πh(πx); it follows that (πlπZ)(πx)π≤πh(πx), thus πlπZπ≤πh.

.group
We must also show that πlπZεπF, i.e., that it is continuous.  Let πX⊂πD be a 
chain.  We need
.begin center;
(πlπZ)(πlπX) = πl{(πlπZ)(πx) | πxεπX}
.end
.begin tabit2 (15,40);

(πlπZ)(πlπX) = (?λ%2x.πl{%2f(x) | f∩επZ})(πlπX)\\definition of πlπZ
\= πl{πf(πl%2X) | f∩επZ}\by function application in πF
\= πl{πl{%2f(x) |x∩επX} | πfεπZ}\by continuity of πf's
\= πl{%2f(x) | f∩επZ, πxεπX}
\= πl{(πl%2Z)(x) | x∩επX}
.end
.end
.end


The next theorem ensures the existence of the least fixed point operator
πY:[πD→πD]→πD; and that πY is continuous, that is, πYε[[πD→πD]→πD].

%7THEOREM 3∩
.begin indent 10,10;
a)  For any CPO πD, every πfε[πD→πD] has a minimum fixed point πYπfεπD, i.e.,
 %2f(Yf)#=#Yf∩ and for all πxεπD %2f(x)=x => Yfπ≤πx.

b) πY is continuous, so πYε[[πD→πD]→πD].
.end
For proof see Milner [10].



.SS(The Models,,)
.begin "on |]"
.at "|"⊂"%f)%1"⊃
We shall now look at the models for LCF.  For intelligibility and compactness
of notation, we sometimes write terms of the form ⊃%d(s)(t)(u)∩ and ∪Y(λx.s)∩
respectively as ∪(s∩→∪t,u)∩ and ∪(αx.s)∩⊗↓∪α∩ acts like the Label operator
in LISP.←, and dispense with ⊃ and ∪Y∩.

.turnoff "{", "}","∪";
A %3⊗→standard model↔←∩ of LCF is a family {πD↓β} of CPO's, one for each type β,
where πD↓i is an arbitrary CPO, πD↓t is the CPO {!t, !f, ⊗b↓t} under the 
partial order given by the diagram:
.begin nofill;

			!t		!f



				⊗b↓t

.end
and πD↓12 = [πD↓1→πD↓2].  Note that πD↓i completely determines a standard
model.

Let $I be the set of identifiers of LCF.  A %3⊗→standard interpretation↔←∩ (of LCF)
is a standard model {πD↓β} together with a %3⊗→standard assignment↔←∩, which is
a function 
.begin center;
⊗→%6A%1↔←:$I→πll{πD↓β}  which satisfies the conditions
.end
.turnon "{", "}", "∪";
.begin indent 10,10; nofill;
1)  $A?x:β| ε πD↓β

2)  The value of ?A for the special identifiers is given by the following:
    $A⊗T| = !t
    $A⊗F| = !f
    $A⊗U↓β| = ⊗b↓β
    $A⊃↓tβ| = ?λ!xεπD↓t∪.λ∩?hεπD↓β∪.λ!gεπD↓β∪.(!x→?h,!g∪)∩
    $A⊗Y↓3β| = πY↓3β

.fill
where ∪(!x→?h,!g∪)∩, the conditional, takes values ⊗b, ?h, !g as !x#=⊗b↓t,#!t,#!f,
respectively, and where we have subscripted the fixed point operator πY on the
right to indicate that it belongs to the CPO [[πD↓β→πD↓β]→πD↓β].  Note that the ?Y
on the left is an identifier, and the πY on the right is a function.  Theorem
3b) assures us that $A?Y| is continuous, $A⊃| is also a continuous function.

.end

If ?A satisfies condition 1) above, but not necessarily  condition 2), we call it
just an %3assignment∩ yielding an %3interpretation∩ (not necessarily standard).  We
also confuse the terms assignment and interpretation, since we will not be discussing
different standard models.

We write ?A[!x/?x] to indicate the assignment differing from ?A only in that its
value at ?x is !x.  Similarly to the rule we had for environments in ?λ-calculus,
we have
.begin nofill;
					?A[?h/?y]	  if ∪x=y∩
		(?A[!x/?x])[?h/?y] =
					(?A[?h/?y])[!x/?x]   otherwise

	We will write ?A[!x/?x][?h/?y] for (?A[!x/?x])[?h/?y].
.end

We now show how to extend the domain of an assignment ?A to all terms, preserving
the condition that $A?s:β|#ε#πD↓β, which states not only that ?A respects types,
but also that (for composite types) it yields a "continuous" function over the
appropriate domains.

We define ?A by induction on the structure of terms:
.begin nofill; indent 20,20;
$A∪s(t)∩| = $A?s|($A?t|)
$A∪(λx.s)∩| = ?λ!x.(?A[!x/?x])%f(∪s∩|

.end

That ?A respects types is obvious, that it yields a continuous function over
the appropriate domains is a corollary of the following theorem.

%7THEOREM 4∩  For each assignment ?A and for each ?x:β1, ?s:β2,
.begin center;
(?λ!xεπD↓1.(?A[!x/?x])%f(∪s∩|) ε [πD↓1→πD↓2].
.end

For proof see Milner [10].


%7Corollary 4.1∩  For every assignment ?A, type β, and term ?s:β, $A?s| ε πD↓β.
.begin nofill; 
Proof:
	For atomic terms the corollary is assured by the definition of an assignment.
	For ?λ-terms, Theorem 4 gives the corollary.
	For an application ∪s(t):∩β, the Theorem says that
             ?λ!xεπD↓1.(?A[!x/?x])%f(∪s(t)∩| ε [πD↓1→πD↓β],
	     so by application to $A?x| we get
	     ?A∪[$A?x|/?x∪]%f(∪s(t)∩| ε πD↓β; thus
	     $A∪s(t)∩| = ?A∪[$A?x|/?x∪]%f(∪s(t)∩| ε πD↓β  as required.

.end

Now we extend the domain of assignments to include wffs and sentences.

Let ∪s,t∩:β be terms, we add the truth values !T, and !F to the range of an
assignment, and define the assignment of awffs by
.begin nofill;

.group
				!T    if $A∪s∩|?≤$A?t|
		$A?s≤?t| =

				!F    otherwise
.apart

.group
Using πP to denote an arbitrary wff:

				!T    if %eA∩επP => $A%eA∩| = !T
		$AπP|  =
				!F    otherwise

Thus, one might think of a wff as the conjunction of its awffs.
.apart

.group
				!F    if $AπP| = !T, $AπQ| = !F
            $AπP$επQ|  =
				!T    otherwise

.end

We say that πP$επQ is false in ?A, true in ?A, respectively.  A sentence is
%3valid∩ iff it is true in all standard interpretations.
.apart

Next, we would like to show that the rules of inference preserve validity.  The
proofs rely on two facts about assignments which we will not prove.  

First,
if %eA∩ is any syntactic entity in the domain of an assignment ?A, and ?x is
not free in %eA∩, then (?A[!x/?x])%f(%eA∩|#=#$A%eA∩|. 

.R21:
 Secondly, we use the
fact that $A[∪t/x]%eA∩|#=#(?A∪[$A?t|/?x∪])%f(%eA∩|.  (The Substitution Lemma for LCF)


%7THEOREM 5∩  The rules of inference of LCF are valid, i.e., whenever the hypotheses
of a rule are valid, its conclusion is also valid.
.begin tabit2 (7,20);
Proof:
.group
\INCL\If πQ⊂πP, then πP$επQ
.begin fill; indent 20, 20;
πP and πQ are sets of awffs, which can be considered as the conjunction of their
elements.  If πP is true then every awff in πP is true, thus every subset of πP
is also true.
.end
.apart

.group
\\πP$επQ1   πP$επQ2
\CONJ\--------------    clearly valid
\\  πP$επQ1πllπQ2
.apart

.group
\\πP1$επP2   πP2$επP3
\CUT\---------------   clearly valid 
\\   πP1$επP3
.apart

.group
\APPL\?t≤?u$ε∪s(t)∩≤∪s(u)∩
\\   If $A?t|?≤$A?u|, then
\\   $A∪s(t)∩| = $A?s|($A?t|) ?≤ $A?s|($A?u|) = $A∪s(u)∩|
\\   by the monotonicity of $A?s| which is continuous by Theorem 4.
.apart

\REFL\$ε?s≤?s     (by reflexivity of ?≤)

\TRANS\?s≤?t, ?t≤?u $ε ?s≤?u     (by transitivity of ?≤)

\MIN1\$ε⊗U≤?s     (by minimality of ⊗b↓β)

\MIN2\$ε⊗U(?s)≤⊗U    (by definition ⊗b↓12=?λ!xεπD↓1.⊗b↓2)

\CONDT\$ε⊃∪(⊗T∪)(s)(t)=s∩

\CONDU\$ε⊃∪(⊗U∪)(s)(t)=⊗U     	by the standard interpretation of "⊃"

\CONDF\$ε⊃∪(⊗F∪)(s)(t)=t∩

.group
\\    πP$ε?s≤?t
\ABSTR\----------------     x not free in πP
\\πP$ε(∪λx.s)∩≤∪(λx.t)∩
\\   Let ?A be such that $AπP|=!T.  Since ?x is not free in πP, we have
\\   $AπP| = ∪(?A∪[!x∪/x])%f(πP|.
\\   Thus the hypotheses assure us that for each !x in πD↓β, where ?x:β,
\\   (?A∪[!x∪/x])%f(?s| ?≤ ∪(?A∪[!x∪/x])%f(?t|.
\\   Hence ?λ!x∪.(?A∪[!x∪/x])%f(?s| ?≤ ∪λ!x∪.(?A∪[!x∪/x])%f(?t|, that is,
\\   $A∪(λx.s)∩≤∪(λx.t)∩| = !T
.apart

.group
\CONV\$ε∪(λx.s)(t) = [t/x]s∩
\\   $A∪(λx.s)(t)∩| = ∪(λ!x∪.(?A∪[!x∪/x])%f(?s|∪)($A?t|∪)∩   definition of ?A
\\   = ∪(?A∪[$A?t|∪/x])%f(?s|    function application in the domain
\\   = $A∪[t/x]s∩|     by the second fact about assignments, {yon (R21)}
.apart

.group
\ETACONV\$ε∪(λx.yx)=y,   y∩ distinct from ?x
\\   $A∪(λx.yx)∩| = ∪λ!x∪.(?A∪[!x∪/x])%f(∪yx∩|
\\   = ?λ!x∪.(?A∪[!x∪/x])%f(?y|∪((?A∪[!x∪/x])%f(?x|∪)∩     by definition of ?A
\\   = ?λ!x∪.$A?y|(!x)     since ?x does not occur in ?y and def. of ?A
\\   = $A?y|     extensionality in the model (?λ!x was introduced as abbrev.)
.apart

.group
\\πP, ?s=⊗T $ε πQ     πP, ?s=⊗U $ε πQ     πP, ?s=⊗F $ε πQ
\CASES\---------------------------------------------
\\                   πP$επQ
.begin fill; indent 20,20;
Let ?A be such that $AπP| = !T.  Since ?s:⊗t, $A?s| must be !t, ⊗b↓t, or !f, so
one of $A?s=⊗T|, $A?s=⊗U|, $A?s=⊗F| must take value !T.  The validity of the
hypothesis ensures that $AπQ|=!T.
.end
.apart

\FIXP\$ε∪Yx = x(Yx)∩     this is clear by the standard interpretation of ?Y

.group
\\πP$ε∪[⊗U∪/x]πQ    πPπllπQ$ε∪[s(x)/x]πQ
\INDUCT\--------------------------------    where ?x is not free in πP or ?s
\\       πP$ε∪[Ys/x]πQ
.begin fill; indent 20,20;
We consider just the case where πQ is an awff.  Moreover we can assume that it is 
of the form ∪t(x)∩≤∪u(x)∩ where ?x is not free in ?t or ?u, since for any term
?t', $A?t'|#=#$A∪(λy.[y/x]t')(x)∩|, ?y distinct from ?x, and then ?x is not
free in ∪(λy.[y/x]t')∩.
.apart

.group
Let ?A be a standard assignment, $AπP|=!T, and assume that $A?s|=πf, $A?t|=%2g∩,
$A?u|=πh.  We show, by induction on i, that for each i≥0,
.begin center;
%2g(f%8i∩(⊗b↓β)) ?≤ πh(πf%8i∩(⊗b↓β)), where ?x:β.
.apart
.end
.end
.group
\\For i=0,  the first hypothesis gives us that ∪(?A∪[⊗b↓β∪/x])%f(πQ|=!T
\\that is, $A?t|(⊗b↓β)?≤$A?u|(⊗b↓β), since ?x is not free in ?t or ?u,
\\so %2g(⊗b↓β)?≤πh(⊗b↓β)
.apart

.group
\\assume true for i,
\\∪(?A∪[πf%8i∩(⊗b↓β)∪/x])%f(πQ|=!T.  Since ?x is not free in πP, we also have
\\∪(?A∪[πf%8i∩(⊗b↓β)∪/x])%f(πP|=!T.  We deduce from the second hypothesis that
\\∪(?A∪[πf%8i∩(⊗b↓β)∪/x])%f(∪[s(x)/x]πQ|=!T.  Then by the definition of ?A
\\∪(?A∪[πf%8i∩(⊗b↓β)∪/x])%f(∪s(x)∩|=πf(πf%8i∩(⊗b↓β)), since ?x is not free in ?s
\\= πf%8i+1∩(⊗b↓β) so, from the second fact we assumed for assignments we get
\\∪(?A∪[πf%8i+1∩(⊗b↓β)∪/x])%f(πQ|=!T, that is,
\\%2g(f%8i+1∩(⊗b↓β))?≤πh(πf%8i+1∩(⊗b↓β)), which completes the induction.
.apart

.group
.begin turnoff "{", "}";
\\Now, $A∪[Ys/x]πQ|=∪(?A%2[Yf∪/x])%f(πQ|, (recalling that $A?s|=πf) 
\\which we are requiring to have value !T.  That is, we want
\\%2g(Yf)?≤%2h(Yf).
\\%2g(Yf) = πl{%2g(f%8i∩(⊗b↓β)) : i≥0}  by continuity of %2g∩
\\?≤ πl{πh(πf%8i∩(⊗b↓β)) : i≥0}   by the inductive proof above
\\= πh∪(πl{πf%8i∩(⊗b↓β) : i≥0}   by continuity of πh
\\= %2h(Yf)∩  by definition of πY
.apart
.end

.end

Therefore, any sentence which is deducible in the formalism is valid, i.e., we have
a model of the formal system.  This model (as any model would) ensures us
that LCF is a consistent theory.

In placing type constraints on ?λ-terms, we have lost the fixed point operator
∪λf.(λx.f(xx))(λx.f(xx))∩ because ∪(xx)∩ cannot be consistently typed.  However,
we know (Theorem 3) that every function πfε∪[πD→πD∪]∩ does have a minimum
fixed point %2Yf∩επD.  Thus we have made ?Y in the formal system an identifier,
which under every standard interpretation is assigned the value of the
fixed point operator of the appropriate domain.

.end "on |]"